IdLnk $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$:Id $\times$ (:Id $\times$ Id)